package jtg.solver;

import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.Expr;
import com.microsoft.z3.Solver;
import jtg.generator.bean.ConverJimpleVar;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Set;

public class Z3Solver {

    public static String solve(String str, ArrayList<ConverJimpleVar> converJimpleVars) throws Exception {
        // 用于存储声明的布尔变量的集合
        Set<String> declareBools = new HashSet<>();
        // 用于存储表达式中的变量列表
        Set<Expr> varList = new HashSet<>();
        // 创建表达式解析器
        ExpressionEvaluator expressionEvaluator = new ExpressionEvaluator();

        // 解析一个表达式，得到stirng表示的一个断言，这个断言是布尔表达式
        String asserts = expressionEvaluator.buildExpression(str, declareBools);
        ///////////////////////////////////////////////////////////////////////////////
        // 配置SMT求解器
        // SMT 求解器被用来解决布尔表达式的路径约束，判断是否存在满足条件的输入。
        // 它通过 Z3 SMT 求解器来实现，该求解器是一种常用的开源 SMT 求解器。
        HashMap<String, String> cfg = new HashMap<String, String>();
        cfg.put("model", "true");
        // 一个运行环境（context），用于管理 Z3 的主要配置、内部状态以及资源分配。
        Context ctx = new Context(cfg);
        Solver s = ctx.mkSolver();
        StringBuilder exprs = new StringBuilder();
        for (String expr : declareBools){
            exprs.append(expr);
            String temp = expr.replaceAll("\\(declare-const ", "").replaceAll(" Real\\)","");
            varList.add(ctx.mkRealConst(temp));
        }
        BoolExpr boolExpr = ctx.parseSMTLIB2String(exprs.toString()+asserts,null,null,null,null)[0];
        s.add(boolExpr);
        StringBuilder res = new StringBuilder();
        try {
            String status = s.check().toString();
            if (status.equals("SATISFIABLE")) {
                for (Expr var : varList) {
                    // 先解出来
                    String evalString = s.getModel().eval(var, false).toString();
                    ////////////////////处理有强制类型转换的参数////////////////////////
                    evalString = switchToOriType(converJimpleVars, var, evalString);
                    ////////////////////////////////////////////////////////////////
                    res.append(var + "=" + evalString + " ");
                }
            } else {
                res.append("无解");//无解
            }

        }catch (Exception e){
            res.append(e);
        }
        //System.out.println(res.toString());
        return res.toString();
    }

    /**
     * 处理类型转换，把所有不是数字型的变量转换回原来类型
     * @param converJimpleVars 已存好的类型转换
     * @param var 求解的变量
     * @param evalString 所求解
     */
    private static String switchToOriType(ArrayList<ConverJimpleVar> converJimpleVars, Expr var, String evalString ) {
        String evalStringAft = evalString;
        for (int i = 0; i < converJimpleVars.size(); i++) {
            ConverJimpleVar jVar = converJimpleVars.get(i);
            if (jVar.getVar().equals(var.toString())) {
                // 如果原来是char类型
                if (jVar.getOriginalType().equals("char")) {
                    // Expr -> int -> char -> String
                    int evalInt = Integer.parseInt(evalString);
                    if (evalInt > 0) evalStringAft = Character.toString((char) evalInt);
                        // 说明这个解析器直接给了0，但是他的ASCII编码是Null，所以要避免这个值，直接设成0？
                    else if (evalInt == 0) evalStringAft = Character.toString((char) (evalInt+48));
                    else throw new ExpressionException("char类型处理出错");
                    converJimpleVars.remove(jVar);
                    i--;
                }
                // 原来是Byte
                else if (jVar.getOriginalType().equals("byte") || jVar.getOriginalType().equals("java.lang.Byte")) {
                    Byte evalByte = Byte.parseByte(evalString);
                    evalStringAft = String.valueOf(evalByte);
                    converJimpleVars.remove(jVar);
                    i--;
                }
                // 原来是short问题
                else if (jVar.getOriginalType().equals("short")) {
                    short evalShort = Short.parseShort(evalString);
                    evalStringAft = String.valueOf(evalShort);
                    converJimpleVars.remove(jVar);
                    i--;
                }
                // 原来是boolean问题
                else if (jVar.getOriginalType().equals("boolean")) {
                    if (evalString.compareTo("0") <= 0)
                        evalStringAft = "false";
                    else evalStringAft = "true";
                }
                // 原来是String类型
                else if (jVar.getOriginalType().equals("java.lang.String")) {
                    // 前面把
                }
            }
        }
        return evalStringAft;
    }
}
